package com.um2.qualite;

/**
 * @version 1.0 
 * @author Halot Sebastien
 * @author Jean-Marie Codol 
 * This is a disk of a Hanoi tower, 
 * Specification we decided that the disk must have a maximum size of 10
 */
public class Disk implements Comparable {

	
    private int size;

    //@public model int disksize;
    //@private represents disksize <- this.size ;

    /**
     * Create a new Disk
     * @param t the size of the disk (a natural) it must be in [1..10]
     */
    /*@
      @ requires t>0; 
      @ requires t<10; 
      @ ensures this.disksize==t; 
      @*/
    public Disk(int t) {
        this.size = t;
    }

    /**
     * Compare this Disk with an other
     * 
     * @param o  the Disk to compare with
     * @return 1 if o is the bigger, 0 if this disk and o are the same, -1 if o is the smaller
     */
    //@ also
    //@ requires (o instanceof Disk);
    //@ ensures \result==0 || \result==1 || \result==-1 ; 
    public /*@ pure @*/ int compareTo(Object o) {

        int osize = ((Disk) o).getSize();
        int result = 12;
        if (osize > this.getSize()) {
            result = 1;
        } else if (osize == this.getSize()) {
            result = 0;
        } else {
            result = -1;
        }
        return result;

    }

    /**
     * @return the size of the disk
     */
    /*@ 
      @ ensures this.disksize>0;
      @ ensures this.disksize<10; 
      @ ensures \result==this.disksize;
      @*/
    public int getSize() {
        return this.size;
    }

    /**
     * @return a string to represent this disk, this string will be composed with as many "X" characters as this disk size
     * "" cannot be return because a disk minimum size is 1.
     */
    
    /*@ also
      @ requires this.disksize>0;
      @ requires this.disksize<10;
      @ ensures \result !=""; 
      @ ensures \result.length()==this.disksize;
      @*/
    
    public String toString() {
        String result = "";
        for (int i = 0; i < this.getSize(); i++) {
            result += "X";
        }
        return result;
    }

}
